MAYBE
* Step 1: Failure MAYBE
  + Considered Problem:
      - Strict TRS:
          'add('0(),y) -> y
          'add('neg('s('0())),y) -> 'pred(y)
          'add('neg('s('s(x))),y) -> 'pred('add('pos('s(x)),y))
          'add('pos('s('0())),y) -> 'succ(y)
          'add('pos('s('s(x))),y) -> 'succ('add('pos('s(x)),y))
          'and('false(),'false()) -> 'false()
          'and('false(),'true()) -> 'false()
          'and('true(),'false()) -> 'false()
          'and('true(),'true()) -> 'true()
          'div('0(),'0()) -> 'divByZero()
          'div('0(),'neg(y)) -> '0()
          'div('0(),'pos(y)) -> '0()
          'div('neg(x),'0()) -> 'divByZero()
          'div('neg(x),'neg(y)) -> 'positive('natdiv(x,y))
          'div('neg(x),'pos(y)) -> 'negative('natdiv(x,y))
          'div('pos(x),'0()) -> 'divByZero()
          'div('pos(x),'neg(y)) -> 'negative('natdiv(x,y))
          'div('pos(x),'pos(y)) -> 'positive('natdiv(x,y))
          'divsub('0(),'0()) -> '0()
          'divsub('0(),'s(y)) -> 'underflow()
          'divsub('s(x),'0()) -> 's(x)
          'divsub('s(x),'s(y)) -> 'divsub(x,y)
          'eq('0(),'0()) -> 'true()
          'eq('0(),'neg(y)) -> 'false()
          'eq('0(),'pos(y)) -> 'false()
          'eq('0(),'s(y)) -> 'false()
          'eq('neg(x),'0()) -> 'false()
          'eq('neg(x),'neg(y)) -> 'eq(x,y)
          'eq('neg(x),'pos(y)) -> 'false()
          'eq('pos(x),'0()) -> 'false()
          'eq('pos(x),'neg(y)) -> 'false()
          'eq('pos(x),'pos(y)) -> 'eq(x,y)
          'eq('s(x),'0()) -> 'false()
          'eq('s(x),'s(y)) -> 'eq(x,y)
          'eq(dd(x'1,x'2),dd(y'1,y'2)) -> 'and('eq(x'1,y'1),'eq(x'2,y'2))
          'eq(dd(x'1,x'2),nil()) -> 'false()
          'eq(nil(),dd(y'1,y'2)) -> 'false()
          'eq(nil(),nil()) -> 'true()
          'equal(x,y) -> 'eq(x,y)
          'mod(x,y) -> 'sub(x,'mult(y,'div(x,y)))
          'mult('0(),'0()) -> '0()
          'mult('0(),'neg(y)) -> '0()
          'mult('0(),'pos(y)) -> '0()
          'mult('neg(x),'0()) -> '0()
          'mult('neg(x),'neg(y)) -> 'pos('natmult(x,y))
          'mult('neg(x),'pos(y)) -> 'neg('natmult(x,y))
          'mult('pos(x),'0()) -> '0()
          'mult('pos(x),'neg(y)) -> 'neg('natmult(x,y))
          'mult('pos(x),'pos(y)) -> 'pos('natmult(x,y))
          'natadd('0(),y) -> y
          'natadd('s(x),y) -> 's('natadd(x,y))
          'natdiv('0(),'0()) -> 'divByZero()
          'natdiv('0(),'s(y)) -> '0()
          'natdiv('s(x),'0()) -> 'divByZero()
          'natdiv('s(x),'s(y)) -> 'natdiv'('divsub(x,y),'s(y))
          'natdiv('underflow(),y) -> '0()
          'natdiv'('0(),y) -> 's('0())
          'natdiv'('s(x),y) -> 's('natdiv('s(x),y))
          'natdiv'('underflow(),y) -> '0()
          'natmult('0(),y) -> '0()
          'natmult('s(x),y) -> 'natadd(y,'natmult(x,y))
          'natsub('0(),'0()) -> '0()
          'natsub('0(),'s(y)) -> '0()
          'natsub('s(x),'0()) -> 's(x)
          'natsub('s(x),'s(y)) -> 'natsub(x,y)
          'negative('0()) -> '0()
          'negative('neg(x)) -> 'pos(x)
          'negative('pos(x)) -> 'neg(x)
          'negative('s(x)) -> 'neg('s(x))
          'positive('0()) -> '0()
          'positive('neg(x)) -> 'neg(x)
          'positive('pos(x)) -> 'pos(x)
          'positive('s(x)) -> 'pos('s(x))
          'pred('0()) -> 'neg('s('0()))
          'pred('neg('s(x))) -> 'neg('s('s(x)))
          'pred('pos('s('0()))) -> '0()
          'pred('pos('s('s(x)))) -> 'pos('s(x))
          'sub(x,'0()) -> x
          'sub(x,'neg(y)) -> 'add(x,'pos(y))
          'sub(x,'pos(y)) -> 'add(x,'neg(y))
          'succ('0()) -> 'pos('s('0()))
          'succ('neg('s('0()))) -> '0()
          'succ('neg('s('s(x)))) -> 'neg('s(x))
          'succ('pos('s(x))) -> 'pos('s('s(x)))
          eratos(dd(x,xs)) -> dd(x,eratos(filter(x,xs)))
          eratos(nil()) -> nil()
          filter(p,dd(x,xs)) -> filter'('equal('mod(x,p),'0()),x,filter(p,xs))
          filter(p,nil()) -> nil()
          filter'('false(),x,xs) -> dd(x,xs)
          filter'('true(),x,xs) -> xs
      - Signature:
          {'add/2,'and/2,'div/2,'divsub/2,'eq/2,'equal/2,'mod/2,'mult/2,'natadd/2,'natdiv/2,'natdiv'/2,'natmult/2
          ,'natsub/2,'negative/1,'positive/1,'pred/1,'sub/2,'succ/1,eratos/1,filter/2,filter'/3} / {'0/0,'divByZero/0
          ,'false/0,'neg/1,'pos/1,'s/1,'true/0,'underflow/0,dd/2,nil/0}
      - Obligation:
          innermost runtime complexity wrt. defined symbols {'add,'and,'div,'divsub,'eq,'equal,'mod,'mult,'natadd
          ,'natdiv,'natdiv','natmult,'natsub,'negative,'positive,'pred,'sub,'succ,eratos,filter
          ,filter'} and constructors {'0,'divByZero,'false,'neg,'pos,'s,'true,'underflow,dd,nil}
  + Applied Processor:
      EmptyProcessor
  + Details:
      The problem is still open.
MAYBE